Inference at * 
Iof proof for Lemma p-fun-exp-one:


  A:Type, f:(A(A + Top)). f^1 = f 

latex

 by ((RepUR ``p-fun-exp`` ( 0)) 
CollapseTHEN (Auto)) 
CollapseTHEN ((BLemma `p-compose-id`) 

CoCollapseTHEN (Auto)) 

latex

C.

Definitions	f^n, Type, s = t, x:AB(x), left + right, Top, x:A. B(x), t  T
Lemmas	p-compose-id